$\forall$$T$:Type, $l_{1}$, $l_{2}$, $l_{3}$:$T$ List. $l_{1}$ $\leq$ $l_{2}$ @ $l_{3}$ $\Rightarrow$ $\parallel$$l_{1}$$\parallel\leq\parallel$$l_{2}$$\parallel$ $\Rightarrow$ $l_{1}$ $\leq$ $l_{2}$